Inference at * 
Iof proof for Lemma simplify-equal-imp:


  T:Type, x, y, z:T. ((y = z))  (((x = y)  (x = z))  ((x = y))) 

latex

 by Auto  
THEN ParallelOp (-2) 
THEN ThinTrivial THEN Auto 

latex

TH.

Definitions	P  Q, P & Q, P  Q, x:A. B(x), , t  T, A, False, P  Q
Lemmas	not wf